$\forall$${\it es}$:event\_system\{i:l\}, $e$:es{-}E(${\it es}$). es\_state\_after(${\it es}$; $e$) $\in$ es\_state(${\it es}$; loc($e$))